perm filename MINIMA.XGP[F76,JMC]1 blob
sn#251096 filedate 1976-12-01 generic text, type T, neo UTF8
/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30
␈↓ α∧␈↓␈↓ εddraft
␈↓ α∧␈↓α␈↓ β$MINIMAL INFERENCE - A WAY OF JUMPING TO CONCLUSIONS
␈↓ α∧␈↓Abstract:␈αHumans␈αand␈αintelligent␈αcomputer␈αprograms␈αmust␈αoften␈αjump␈αto␈αthe␈αconclusion␈α
that␈αthe
␈↓ α∧␈↓objects␈αthey␈αknow␈αabout␈αare␈αthe␈αonly␈αrelevant␈αobjects␈αinvolved␈αin␈αa␈αproblem.␈α
␈↓↓Minimal␈αinference␈↓
␈↓ α∧␈↓is a formalization of this mode of approximate reasoning.
␈↓ α∧␈↓␈↓ ε|1␈↓ ∧
␈↓ α∧␈↓␈↓ εddraft␈↓ u2
␈↓ α∧␈↓αMINIMAL ENTAILMENT
␈↓ α∧␈↓␈↓ αT␈↓↓Minimal␈α⊂reasoning␈↓␈α⊂has␈α⊂a␈α⊂semantic␈α⊂form␈α⊂called␈α⊂␈↓↓minimal␈α⊂entailment␈↓␈α⊂and␈α⊂a␈α⊃syntactic␈α⊂form
␈↓ α∧␈↓called ␈↓↓minimal inference␈↓. We begin with ␈↓↓minimal entailment␈↓.
␈↓ α∧␈↓␈↓ αTLet␈α
␈↓↓A␈↓␈α
be␈α
a␈α
set␈α
of␈α
sentences␈α
of␈α
first␈α
order␈α
logic␈α
and␈α
␈↓↓p␈↓␈α
a␈α
sentence.␈α
As␈α
is␈α
customary␈α
in␈α
logic,␈α
we
␈↓ α∧␈↓say␈αthat␈α
␈↓↓A␈αentails␈αp␈↓␈α
(written␈α␈↓↓A␈α␈↓πq␈↓↓␈α
p␈↓)␈αiff␈α␈↓↓p␈↓␈α
is␈αtrue␈αin␈α
all␈αmodels␈αof␈α
␈↓↓A.␈↓␈αSuppose␈α␈↓↓M1␈↓␈α
and␈α␈↓↓M2␈↓␈αare␈α
two
␈↓ α∧␈↓models␈αof␈αa␈αset␈α
of␈αsentences␈αin␈αa␈α
multi-sorted␈αlogic.␈α We␈αsay␈αthat␈α
␈↓↓M2␈↓␈αextends␈α␈↓↓M1␈↓␈α(written␈α
␈↓↓M1␈α≤
␈↓ α∧␈↓↓M2␈↓)␈α⊗iff␈α⊗␈↓↓domain(M1)␈α↔⊂␈α⊗domain(M2)␈↓,␈α⊗but␈α↔the␈α⊗predicates␈α⊗when␈α↔applied␈α⊗to␈α⊗the␈α↔elements␈α⊗of
␈↓ α∧␈↓␈↓↓domain(M1)␈↓␈αhave␈αthe␈αsame␈αvalues␈αin␈α␈↓↓M2␈↓␈αthat␈αthey␈αhave␈αin␈α␈↓↓M1.␈↓␈α␈↓↓M␈↓␈αis␈αcalled␈αa␈αminimal␈αmodel␈αof
␈↓ α∧␈↓␈↓↓A␈↓␈αiff␈αit␈αis␈αnot␈αa␈αproper␈αextension␈αof␈αanother␈αmodel.␈α We␈αsay␈αthat␈α␈↓↓A␈↓␈α␈↓↓minimally␈αentails␈αp␈↓␈α(written␈α␈↓↓A
␈↓ α∧␈↓↓␈↓πq␈↓βm␈↓↓ p␈↓) iff ␈↓↓p␈↓ is true in all minimal models of ␈↓↓A.␈↓
␈↓ α∧␈↓␈↓ αTWe␈α⊂first␈α⊂show␈α⊂that␈α⊃minimal␈α⊂entailment␈α⊂is␈α⊂not␈α⊃equivalent␈α⊂to␈α⊂ordinary␈α⊂entailment␈α⊃in␈α⊂any
␈↓ α∧␈↓logical␈αsystem␈αor␈αto␈αany␈αform␈αof␈αdeduction.␈α For␈αany␈αform␈αof␈αdeduction,␈αif␈α␈↓↓A␈α␈↓πr␈↓↓␈αp␈↓␈αand␈α␈↓↓A␈α⊂␈αB␈↓,␈αthen
␈↓ α∧␈↓␈↓↓B␈α
␈↓πr␈↓↓␈α
p␈↓.␈α We␈α
may␈α
call␈α
this␈αproperty␈α
␈↓↓monotonicity␈↓.␈α
Exactly␈αthe␈α
same␈α
proof␈α
that␈αproved␈α
␈↓↓p␈↓␈α
from␈α␈↓↓A␈↓␈α
will
␈↓ α∧␈↓prove␈αit␈α
from␈α␈↓↓B.␈↓␈αEntailment␈α
also␈αhas␈αthis␈α
property;␈αif␈α␈↓↓p␈↓␈α
is␈αtrue␈α
in␈αall␈αmodels␈α
of␈α␈↓↓A,␈↓␈αit␈α
is␈αtrue␈αin␈α
all
␈↓ α∧␈↓models␈αof␈α␈↓↓B,␈↓␈αbecause␈αthe␈αlatter␈αare␈αa␈αsubset␈αof␈αthe␈αmodels␈αof␈α␈↓↓A.␈↓␈αHowever,␈αminimal␈αentailment␈αis
␈↓ α∧␈↓not␈αmonotonic.␈α
Namely,␈αconsider␈α
the␈αnull␈α
set␈α␈↓↓N␈↓␈αof␈α
sentences.␈α Its␈α
minimal␈αmodel␈α
is␈αa␈αdomain␈α
with
␈↓ α∧␈↓one␈α
element␈α
(in␈α
most␈αformalizations)␈α
so␈α
that␈α
the␈α
sentence␈α␈↓↓∀x y.x = y␈↓␈α
is␈α
minimally␈α
entailed␈α
by␈α␈↓↓N.␈↓
␈↓ α∧␈↓However,␈αthe␈αset␈α␈↓↓B␈↓␈αconsisting␈αof␈αthe␈αnegation␈αof␈αthis␈αsentence␈αcertainly␈αcontains␈αthe␈αnull␈αset␈α␈↓↓N.␈α ␈↓
␈↓ α∧␈↓Here␈α∂are␈α∂some␈α∂mathematical␈α∂examples.␈α∂ The␈α⊂minimal␈α∂model␈α∂of␈α∂the␈α∂Peano␈α∂axioms␈α⊂without␈α∂the
␈↓ α∧␈↓schema␈α∞of␈α∞induction␈α∞is␈α∞the␈α∞standard␈α∞model␈α∞of␈α∞the␈α∞integers␈α∞provided␈α∞the␈α∞constant␈α∞0␈α∂is␈α∞explicitly
␈↓ α∧␈↓mentioned.␈α The␈αsystem␈αconsisting␈αonly␈αof␈αthe␈αaxioms␈αfor␈αthe␈α␈↓↓successor␈↓␈αoperation␈αomitting␈αaxioms
␈↓ α∧␈↓for␈α0␈α
has␈αno␈αminimal␈α
model,␈αbecause␈αany␈α
model␈αhas␈αa␈α
submodel.␈α There␈αis␈α
also␈αno␈αminimal␈α
model
␈↓ α∧␈↓if␈α
0␈αis␈α
characterized␈α
only␈αby␈α
an␈αexistential␈α
axiom,␈α
␈↓↓∃z.∀x.successor x ≠ z␈↓.␈α The␈α
minimal␈α
model␈αof
␈↓ α∧␈↓the␈α
axioms␈α
for␈α
group␈α
theory␈α
is␈α
the␈α
group␈α
of␈α
one␈α
element.␈α
If␈α
we␈α
add␈α
a␈α
sentence␈α
asserting␈αthat␈α
there
␈↓ α∧␈↓is␈αmore␈αthan␈αone␈αelement,␈αthen␈αthe␈αminimal␈αmodels␈αare␈αthe␈αcyclic␈αgroups␈αof␈αprime␈αorder␈α
and␈αthe
␈↓ α∧␈↓infinite cyclic group.
␈↓ α∧␈↓αMinimal inference.
␈↓ α∧␈↓␈↓ αTMinimal␈αentailment␈α
is␈αa␈αsemantic␈α
mode␈αof␈αreasoning.␈α
As␈αMartin␈αDavis␈α
points␈αout,␈αit␈α
is␈αin
␈↓ α∧␈↓general␈α∩infinitary.␈α⊃ Indeed,␈α∩since␈α⊃the␈α∩minimal␈α∩model␈α⊃of␈α∩the␈α⊃usual␈α∩first␈α⊃order␈α∩axioms␈α∩for␈α⊃the
␈↓ α∧␈↓integers␈αis␈αthe␈α␈↓↓standard␈αmodel␈↓,␈αthe␈αminimal␈αconsequences␈αof␈αthe␈αaxioms␈αare␈αjust␈αthe␈αtrue␈αsentences
␈↓ α∧␈↓of␈α→arithmetic,␈α_and␈α→this␈α_set␈α→isn't␈α_recursively␈α→enumerable␈α_or␈α→even␈α_arithmetic.␈α→ Here␈α→is␈α_a
␈↓ α∧␈↓corresponding␈αsyntactic␈αmode␈αof␈αreasoning.␈α Since␈αby␈αGoedel's␈αtheorem␈αit␈αwon't␈αbe␈αcomplete,␈αthere
␈↓ α∧␈↓will be stronger modes.
␈↓ α∧␈↓␈↓ αTThe␈α
idea␈α
is␈α
to␈α
imitate␈α
the␈α
axiom␈α
schema␈αof␈α
induction.␈α
Let␈α
␈↓↓A␈↓␈α
be␈α
the␈α
conjunction␈α
of␈αa␈α
certain
␈↓ α∧␈↓subset␈α
of␈αour␈α
axioms␈α
called␈αthe␈α
primary␈α
axioms.␈α The␈α
criterion␈α
for␈αcalling␈α
some␈α
axioms␈αprimary
␈↓ α∧␈↓and␈αothers␈αsecondary␈αis␈αnot␈αyet␈αentirely␈αclear,␈αbut␈αit␈αseems␈αclear␈αthat␈αsome␈αseparation␈αis␈αdesirable.
␈↓ α∧␈↓Let␈α␈↓↓A␈↓ ␈↓#
F␈↓#␈↓␈αbe␈αthe␈αresult␈αof␈αrelativizing␈α␈↓↓A␈↓␈αwith␈αrespect␈αto␈αthe␈αpredicate␈αparameter␈α␈↓ F␈↓.␈α (␈↓↓A␈↓ ␈↓#
F␈↓#␈↓␈αis␈αobtained
␈↓ α∧␈↓from␈α␈↓↓A␈↓␈αby␈αreplacing␈αevery␈αuniversal␈αquantifier␈α␈↓↓∀x.␈↓␈αby␈α␈↓↓∀x.␈↓ F␈↓↓(x) ⊃␈↓␈αand␈αevery␈αexistential␈αquantifier
␈↓ α∧␈↓␈↓↓∃x.␈↓␈α⊃by␈α⊃␈↓↓∃x.␈↓ F␈↓↓(x) ∧␈↓.␈α⊃ For␈α⊃each␈α⊃constant␈α⊃␈↓↓a␈↓␈α⊃appearing␈α⊂in␈α⊃␈↓↓A,␈↓␈α⊃we␈α⊃must␈α⊃adjoin␈α⊃␈↓ F␈↓↓(a)␈↓␈α⊃and␈α⊃for␈α⊂each
␈↓ α∧␈↓function symbol ␈↓↓f,␈↓ we must adjoin the axiom ␈↓↓∀x.(␈↓ F␈↓↓(x) ⊃ ␈↓ F␈↓↓(f(x))␈↓)). We introduce the schema
␈↓ α∧␈↓␈↓ ε|2␈↓ ∧
␈↓ α∧␈↓␈↓ εddraft␈↓ u3
␈↓ α∧␈↓␈↓ αT␈↓↓A␈↓ ␈↓#
F␈↓#␈↓↓ ⊃ ∀x.␈↓ F␈↓↓(x)␈↓
␈↓ α∧␈↓which␈α∞we␈α∞call␈α∂␈↓↓the␈α∞minimal␈α∞completion␈α∂schema␈↓␈α∞of␈α∞␈↓↓A␈↓␈α∂and␈α∞write␈α∞␈↓↓MCS(A)␈↓.␈α∂ We␈α∞will␈α∞call␈α∂the␈α∞system
␈↓ α∧␈↓obtained␈αby␈αadjoining␈αthe␈αschema␈α␈↓↓MCS(A)␈↓␈αto␈αthe␈αaxiom␈α␈↓↓A␈↓␈αthe␈α␈↓↓minimal␈αcompletion␈αof␈αA␈↓,␈αwriting␈α
it
␈↓ α∧␈↓␈↓↓MC(A)␈↓.␈α
␈↓↓MCS(A)␈↓␈α
is␈α∞an␈α
attempt␈α
to␈α∞assert␈α
that␈α
the␈α
only␈α∞objects␈α
are␈α
those␈α∞required␈α
to␈α
exist␈α∞by␈α
the
␈↓ α∧␈↓axioms␈α␈↓↓A.␈α ␈↓␈αHere␈αis␈αa␈αtrivial␈αexample␈αof␈αa␈αminimal␈αcompletion.␈α Suppose␈αwe␈αhave␈αa␈αsingle␈αaxiom
␈↓ α∧␈↓␈↓↓ok(a)␈↓ in our primary set. Its relativization will be ␈↓ F␈↓↓(a) ∧ ok(a)␈↓. The minimization schema is then
␈↓ α∧␈↓␈↓ αT␈↓ F␈↓↓(a) ∧ ok(a) ⊃ ∀x.␈↓ F␈↓↓(x)␈↓.
␈↓ α∧␈↓If␈α
we␈αsubstitute␈α
␈↓↓λx.(x = a)␈↓␈αfor␈α
␈↓ F␈↓␈αin␈α
the␈αschema␈α
we␈αcan␈α
conclude␈α␈↓↓∀x.(x = a)␈↓␈α
which␈αcharacterizes␈α
the
␈↓ α∧␈↓minimal␈αmodel␈α
of␈αthat␈αaxiom.␈α
Indeed,␈αMartin␈αDavis␈α
showed␈αme␈αthat␈α
if␈αevery␈αmodel␈α
of␈α␈↓↓A␈↓␈α
has␈αa
␈↓ α∧␈↓minimal␈αsubmodel␈αand␈αa␈αsentence␈α␈↓ f␈↓␈αis␈αtrue␈αin␈αany␈αsupermodel␈αof␈αany␈αmodel␈αof␈α␈↓ f␈↓,␈αthen␈α␈↓ f␈↓␈αis␈αtrue
␈↓ α∧␈↓in all minimal models of ␈↓↓A␈↓ iff it is provable in the minimal completion of ␈↓↓A.␈↓
␈↓ α∧␈↓␈↓ αTLet␈α␈↓↓s1␈↓␈α
be␈αthe␈αsentence␈α
␈↓↓∀x.ok(x) = p␈↓.␈α ␈↓↓p␈↓␈α
is␈αprovable␈αin␈α
␈↓↓MC({ok(a)} ∪ s1␈↓,␈αbut␈α
it␈αis␈αnot␈α
provable
␈↓ α∧␈↓in␈α
␈↓↓MC({ok(a) ∧ s1}␈↓,␈α
because␈α
the␈αlater␈α
admits␈α
minimal␈α
models␈αin␈α
which␈α
␈↓↓p␈↓␈α
is␈αfalse␈α
and␈α
there␈α
is␈αan
␈↓ α∧␈↓individual␈α␈↓↓b␈↓␈αsuch␈αthat␈α␈↓↓¬ok(b).␈↓␈α
Therefore,␈αit␈αseems␈αthat␈αwe␈α
have␈αto␈αdivide␈αour␈αsentences␈α
into␈αtwo
␈↓ α∧␈↓groups␈α
if␈α
we␈α
want␈α
minimal␈αinference␈α
to␈α
be␈α
useful␈α
-␈αa␈α
primary␈α
group␈α
whose␈α
minimal␈αcompletion
␈↓ α∧␈↓we␈α∂form,␈α⊂and␈α∂a␈α⊂secondary␈α∂group␈α⊂which␈α∂is␈α∂used␈α⊂but␈α∂which␈α⊂is␈α∂not␈α⊂completed.␈α∂ The␈α⊂criteria␈α∂for
␈↓ α∧␈↓deciding␈α∞in␈α
which␈α∞group␈α
to␈α∞put␈α
a␈α∞fact␈α
are␈α∞determined␈α
by␈α∞how␈α
we␈α∞want␈α
Occam's␈α∞razor␈α∞to␈α
work.
␈↓ α∧␈↓We hope to clarify this in a later version of this paper.
␈↓ α∧␈↓␈↓ αTWe␈α
can␈α
form␈α
the␈α
minimal␈α
completion␈α
of␈α
the␈α
algebraic␈α
Peano␈α
axioms␈α
as␈α
follows:␈α∞We␈α
write
␈↓ α∧␈↓the axioms
␈↓ α∧␈↓1)␈↓ αt ␈↓↓∀n.n' ≠ 0␈↓,
␈↓ α∧␈↓2)␈↓ αt ␈↓↓∀n.(n')␈↓∧-␈↓↓ = n␈↓,
␈↓ α∧␈↓and
␈↓ α∧␈↓3)␈↓ αt ␈↓↓∀n.(n ≠ 0 ⊃ n␈↓∧-␈↓↓' = n)␈↓,
␈↓ α∧␈↓where␈α⊂␈↓↓n'␈↓␈α⊃denotes␈α⊂the␈α⊂successor␈α⊃of␈α⊂␈↓↓n␈↓␈α⊂and␈α⊃␈↓↓n␈↓∧-␈↓␈α⊂denotes␈α⊂the␈α⊃predecessor␈α⊂of␈α⊂␈↓↓n␈↓.␈α⊃ The␈α⊂minimization
␈↓ α∧␈↓schema of this set of axioms is
␈↓ α∧␈↓4)␈↓ αt␈α
␈↓↓␈↓ F␈↓↓(0)␈α
∧␈α
∀n.(␈↓ F␈↓↓(n)␈α⊃␈α
␈↓ F␈↓↓(n'))␈α
∧␈α
∀n.(␈↓ F␈↓↓(n)␈α⊃␈α
␈↓ F␈↓↓(n␈↓∧-␈↓↓))␈α
∧␈α
∀n.(␈↓ F␈↓↓(n)␈α⊃␈α
n'␈α
≠␈α
0)␈α∧␈α
∀n.(␈↓ F␈↓↓(n)␈α
⊃␈α
(n')␈↓∧-␈↓↓␈α=␈α
n)
␈↓ α∧␈↓↓∧ ∀n.(␈↓ F␈↓↓(n) ⊃ (n≠0 ⊃ (n␈↓∧-␈↓↓)' = n))) ⊃ ∀n.␈↓ F␈↓↓(n)␈↓.
␈↓ α∧␈↓␈↓ αTThis␈αis␈αmuch␈αlonger␈α
than␈αthe␈αusual␈αschema␈α
of␈αinduction,␈αbut␈αcan␈α
be␈αshown␈αequivalent␈αto␈α
it.
␈↓ α∧␈↓Notice␈αthat␈αthe␈αconjuncts␈αin␈αthe␈αpremiss␈αthat␈αrelativize␈αthe␈αaxioms␈α(1)-(3)␈αare␈αredundant;␈αbecause
␈↓ α∧␈↓since␈α∂they␈α∂contain␈α⊂only␈α∂universal␈α∂quantifiers,␈α⊂they␈α∂are␈α∂weaker␈α⊂than␈α∂the␈α∂axioms␈α⊂they␈α∂relativize.
␈↓ α∧␈↓Thus␈αPeano␈αarithmetic␈αis␈αthe␈αminimal␈αcompletion␈αof␈αits␈αalgebraic␈αsubsystem.␈α As␈αusual,␈αwhen␈αthe
␈↓ α∧␈↓axioms␈αadmit␈α
only␈αinfinite␈α
models,␈αthe␈α
schema␈αwill␈α
not␈αbe␈α
sufficient␈αto␈α
enforce␈αthe␈αminimal␈α
model,
␈↓ α∧␈↓and␈αthere␈αwill␈αalso␈αbe␈α␈↓↓non-standard␈↓␈αmodels.␈α Martin␈αDavis␈αhas␈αalso␈αshown␈αthat␈αif␈α0␈αis␈α
introduced
␈↓ α∧␈↓through␈α∞an␈α∞existential␈α∞axiom␈α∞rather␈α∞than␈α∂as␈α∞a␈α∞constant,␈α∞the␈α∞minimal␈α∞completion␈α∂is␈α∞inconsistent;
␈↓ α∧␈↓this corresponds to the fact that this system has no minimal model.
␈↓ α∧␈↓␈↓ ε|3␈↓ ∧
␈↓ α∧␈↓␈↓ εddraft␈↓ u4
␈↓ α∧␈↓αApplications
␈↓ α∧␈↓␈↓ αTWe␈α⊂envisage␈α⊂using␈α⊂minimal␈α⊂inference␈α⊂in␈α⊂AI␈α∂as␈α⊂follows:␈α⊂Suppose␈α⊂a␈α⊂system␈α⊂has␈α⊂a␈α∂certain
␈↓ α∧␈↓collection␈α∞of␈α∞facts.␈α∞ It␈α∞may␈α∞or␈α∂may␈α∞not␈α∞have␈α∞all␈α∞the␈α∞relevant␈α∂facts,␈α∞but␈α∞it␈α∞is␈α∞reasonable␈α∞for␈α∂it␈α∞to
␈↓ α∧␈↓conjecture␈α∞that␈α∞does␈α∞and␈α
examine␈α∞the␈α∞consequences␈α∞of␈α
the␈α∞conjecture.␈α∞ The␈α∞minimal␈α
completion
␈↓ α∧␈↓axiom␈α
for␈αa␈α
set␈α
of␈αstatements␈α
is␈α
an␈αexpression␈α
of␈α
the␈αhypothesis␈α
that␈α
the␈αonly␈α
objects␈α
that␈αexist␈α
are
␈↓ α∧␈↓those␈α⊃which␈α⊂must␈α⊃exist␈α⊂on␈α⊃the␈α⊂basis␈α⊃of␈α⊃these␈α⊂statements.␈α⊃ In␈α⊂order␈α⊃to␈α⊂make␈α⊃this␈α⊃workable␈α⊂in
␈↓ α∧␈↓practice,␈αit␈αwill␈αbe␈αnecessary␈αto␈αapply␈αminimal␈αcompletion␈αto␈αsubsets␈αof␈αthe␈αfacts;␈αdifferent␈αsubsets
␈↓ α∧␈↓will␈αgive␈α
rise␈αto␈α
different␈αconjectures.␈α Moreover,␈α
we␈αwill␈α
need␈αto␈αapply␈α
the␈αrelativization␈α
to␈αonly
␈↓ α∧␈↓some␈α
of␈α∞the␈α
sorts␈α
of␈α∞individuals,␈α
so␈α
that␈α∞we␈α
can␈α
remain␈α∞non-committal␈α
about␈α
whether␈α∞there␈α
are
␈↓ α∧␈↓more of certain sorts than our axioms prove to exist.
␈↓ α∧␈↓␈↓ αTAn␈α∩example␈α∩that␈α∩has␈α∩been␈α∩much␈α∩studied␈α⊃in␈α∩AI␈α∩and␈α∩which␈α∩contains␈α∩enough␈α∩detail␈α⊃to
␈↓ α∧␈↓illustrate various issues is the ␈↓↓missionaries and cannibals␈↓ problem, stated as follows:
␈↓ α∧␈↓␈↓ αT␈↓↓"Three␈α∪missionaries␈α∀and␈α∪three␈α∀cannibals␈α∪come␈α∀to␈α∪a␈α∪river.␈α∀ A␈α∪rowboat␈α∀that␈α∪seats␈α∀two␈α∪is
␈↓ α∧␈↓↓available.␈α
However,␈αif␈α
the␈αcannibals␈α
ever␈αoutnumber␈α
the␈αmissionaries␈α
on␈αeither␈α
bank␈αof␈α
the␈αriver,
␈↓ α∧␈↓↓the outnumbered missionaries will be eaten. How shall they cross the river?"␈↓.
␈↓ α∧␈↓␈↓ αTAmarel␈α⊃(1971)␈α⊃considered␈α⊃various␈α⊃representations␈α⊃of␈α⊃the␈α⊃problem␈α⊃and␈α∩discussed␈α⊃criteria
␈↓ α∧␈↓whereby␈α⊂the␈α⊃following␈α⊂representation␈α⊂is␈α⊃preferred␈α⊂for␈α⊂purposes␈α⊃of␈α⊂AI,␈α⊂because␈α⊃it␈α⊂leads␈α⊃to␈α⊂the
␈↓ α∧␈↓smallest␈αstate␈αspace␈αthat␈αmust␈αbe␈αexplored␈αto␈αfind␈αthe␈αsolution.␈α We␈αrepresent␈αa␈αstate␈αby␈αthe␈α
triplet
␈↓ α∧␈↓consisting␈α∞of␈α∞the␈α
numbers␈α∞of␈α∞missionaries,␈α
cannibals␈α∞and␈α∞boats␈α
on␈α∞the␈α∞initial␈α
bank␈α∞of␈α∞the␈α
river.
␈↓ α∧␈↓The␈αinitial␈αconfiguration␈α
is␈α331,␈αthe␈αdesired␈α
final␈αconfiguration␈αis␈α000,␈α
and␈αone␈αsolution␈α
is␈αgiven
␈↓ α∧␈↓by the sequence (331,220,321,300,311,110,221,020,031,010,021,000) of states.
␈↓ α∧␈↓␈↓ αTWe␈α⊂are␈α⊂not␈α⊂presently␈α⊂concerned␈α⊂with␈α⊂the␈α⊂heuristics␈α⊂of␈α⊂the␈α⊂problem␈α⊂but␈α⊂rather␈α⊂with␈α⊂the
␈↓ α∧␈↓correctness␈αof␈αthe␈αreasoning␈αthat␈α
goes␈αfrom␈αthe␈αEnglish␈αstatement␈α
of␈αthe␈αproblem␈αto␈αAmarel's␈α
state
␈↓ α∧␈↓space␈αrepresentation.␈α
In␈αthe␈α
long␈αrun␈α
we␈αwould␈αlike␈α
a␈αcomputer␈α
to␈αcarry␈α
out␈αthis␈α
reasoning.␈α Of
␈↓ α∧␈↓course␈αthere␈α
are␈αthe␈αwell␈α
known␈αdifficulties␈α
in␈αmaking␈αcomputers␈α
understand␈αEnglish,␈αbut␈α
suppose
␈↓ α∧␈↓the␈α
English␈α
sentences␈α
describing␈α
the␈α
problem␈α
have␈α
already␈α
been␈α
rather␈α
directly␈α
translated␈α
into␈α
first
␈↓ α∧␈↓order␈αlogic.␈α The␈αcorrectness␈αof␈αAmarel's␈αrepresentation␈αis␈αnot␈αan␈αordinary␈αlogical␈αconsequence␈αof
␈↓ α∧␈↓these sentences for two reasons.
␈↓ α∧␈↓␈↓ αTFirst,␈α∞nothing␈α∞has␈α∞been␈α∞stated␈α∞about␈α∞the␈α∞properties␈α∞of␈α∞boats␈α∞or␈α∞even␈α∞the␈α∞fact␈α∞that␈α
rowing
␈↓ α∧␈↓across␈α∞the␈α∞river␈α
doesn't␈α∞change␈α∞the␈α∞numbers␈α
of␈α∞missionaries␈α∞or␈α∞cannibals␈α
or␈α∞the␈α∞capacity␈α∞of␈α
the
␈↓ α∧␈↓boat.␈α These␈αare␈αa␈αconsequence␈αof␈αcommon␈αsense␈αknowledge,␈αso␈αlet␈αus␈αimagine␈αthat␈αcommon␈αsense
␈↓ α∧␈↓knowledge, or at least the relevant part of it, is also expressed in first order logic.
␈↓ α∧␈↓␈↓ αTThe␈α∩second␈α⊃reason␈α∩we␈α⊃can't␈α∩␈↓↓deduce␈↓␈α∩the␈α⊃propriety␈α∩of␈α⊃Amarel's␈α∩representation␈α∩is␈α⊃deeper.
␈↓ α∧␈↓Imagine␈α
giving␈α
someone␈α
the␈α
problem,␈α
and␈α
after␈αhe␈α
puzzles␈α
for␈α
a␈α
while,␈α
he␈α
suggests␈αgoing␈α
upstream
␈↓ α∧␈↓half␈α
a␈α
mile␈α
and␈α
crossing␈α
on␈α
a␈α
bridge.␈α∞ "What␈α
bridge",␈α
you␈α
say.␈α
"No␈α
bridge␈α
is␈α
mentioned␈α∞in␈α
the
␈↓ α∧␈↓statement␈αof␈αthe␈α
problem."␈αAnd␈αthis␈α
dunce␈αreplies,␈α"Well,␈α
it␈αisn't␈αstated␈α
that␈αthere␈αisn't␈α
a␈αbridge".
␈↓ α∧␈↓You␈αlook␈αat␈αthe␈αEnglish␈αand␈αeven␈αat␈αthe␈αtranslation␈αof␈αthe␈αEnglish␈αinto␈αfirst␈αorder␈αlogic,␈αand␈αyou
␈↓ α∧␈↓must␈α∂admit␈α∞that␈α∂it␈α∞isn't␈α∂stated␈α∂that␈α∞there␈α∂is␈α∞no␈α∂bridge.␈α∂ So␈α∞you␈α∂modify␈α∞the␈α∂problem␈α∂to␈α∞exclude
␈↓ α∧␈↓bridges␈α∞and␈α∞pose␈α∂it␈α∞again,␈α∞and␈α∂the␈α∞dunce␈α∞proposes␈α∂a␈α∞helicopter,␈α∞and␈α∂after␈α∞you␈α∞exclude␈α∂that␈α∞he
␈↓ α∧␈↓proposes␈αa␈α
winged␈αhorse␈αor␈α
that␈αthe␈α
others␈αhang␈αonto␈α
the␈αoutside␈α
of␈αthe␈αboat␈α
while␈αtwo␈αrow.␈α
You
␈↓ α∧␈↓␈↓ ε|4␈↓ ∧
␈↓ α∧␈↓␈↓ εddraft␈↓ u5
␈↓ α∧␈↓now␈α
see␈α
that␈α
while␈α
a␈α
dunce,␈α
he␈α
is␈α
an␈αinventive␈α
dunce,␈α
and␈α
you␈α
despair␈α
of␈α
getting␈α
him␈α
to␈αaccept␈α
the
␈↓ α∧␈↓problem␈αin␈α
the␈αproper␈α
puzzler's␈αspirit␈α
and␈αtell␈α
him␈αthe␈α
solution.␈α You␈α
are␈αfurther␈α
annoyed␈αwhen
␈↓ α∧␈↓he␈αattacks␈αyour␈αsolution␈αon␈αthe␈αgrounds␈αthat␈αthe␈αboat␈αmight␈αnot␈αhave␈αoars.␈α After␈αyou␈αrectify␈α
that
␈↓ α∧␈↓omission,␈α
he␈αsuggests␈α
that␈α
a␈αsea␈α
monster␈α
may␈αswim␈α
up␈α
the␈αriver␈α
and␈α
may␈αswallow␈α
the␈αboat.␈α
Again
␈↓ α∧␈↓you are frustrated, and you look for a mode of reasoning that will settle his hash once and for all.
␈↓ α∧␈↓␈↓ αTMinimal␈αmodels␈α
and␈αminimal␈αinference␈α
may␈αgive␈αthe␈α
solution.␈α In␈αa␈α
minimal␈αmodel␈α
of␈αthe
␈↓ α∧␈↓first␈α∞order␈α
logic␈α∞statement␈α
of␈α∞the␈α
problem,␈α∞there␈α∞is␈α
no␈α∞bridge␈α
or␈α∞helicopter.␈α
"Ah",␈α∞you␈α∞say,␈α
"but
␈↓ α∧␈↓there␈αaren't␈αany␈αoars␈αeither".␈α No,␈αwe␈αget␈αout␈αof␈αthat␈αas␈αfollows:␈αIt␈αis␈αa␈αpart␈αof␈αcommon␈αknowledge
␈↓ α∧␈↓that␈αa␈αboat␈αcan␈αbe␈αused␈αto␈αcross␈αa␈αriver␈α␈↓↓unless␈αthere␈αis␈αsomething␈αwrong␈αwith␈αit␈αor␈α
something␈αelse
␈↓ α∧␈↓↓prevents␈αusing␈αit␈↓,␈αand␈αin␈αthe␈αminimal␈αmodel␈αof␈αthe␈αfacts␈αthere␈αdoesn't␈αexist␈αsomething␈αwrong␈α
with
␈↓ α∧␈↓the boat, and there isn't anything else to prevent its use.
␈↓ α∧␈↓␈↓ αTThe␈α∪non-monotonic␈α∩character␈α∪of␈α∩minimal␈α∪reasoning␈α∪is␈α∩just␈α∪what␈α∩we␈α∪want␈α∪here.␈α∩ The
␈↓ α∧␈↓statement,␈α␈↓↓"There␈αis␈αa␈αbridge␈α
a␈αmile␈αupstream."␈↓␈αdoesn't␈αcontradict␈α
the␈αtext␈αof␈αthe␈αproblem,␈α
but␈αits
␈↓ α∧␈↓addition invalidates the Amarel representation.
␈↓ α∧␈↓␈↓ αTAt␈αfirst␈αI␈αconsidered␈αthis␈αsolution␈αtoo␈αad␈αhoc␈αto␈αbe␈αacceptable,␈αbut␈αI␈αam␈αnow␈αconvinced␈αthat
␈↓ α∧␈↓it␈αis␈αa␈αcorrect␈αexplication␈αof␈αthe␈α␈↓↓normal␈↓␈αsituation,␈αe.g.␈αunless␈αsomething␈αabnormal␈αexists,␈αan␈αobject
␈↓ α∧␈↓can be used to carry out its normal function.
␈↓ α∧␈↓␈↓ αTSome␈α∂have␈α∂suggested␈α∂that␈α∂the␈α∂difficulties␈α∂might␈α∂be␈α∂avoided␈α∂by␈α∂introducing␈α∂probabilities.
␈↓ α∧␈↓They␈α∞suggest␈α∞that␈α∞the␈α∂existence␈α∞of␈α∞a␈α∞bridge␈α∞is␈α∂improbable.␈α∞ Well␈α∞the␈α∞whole␈α∂situation␈α∞involving
␈↓ α∧␈↓cannibals␈α∂with␈α⊂the␈α∂postulated␈α⊂properties␈α∂is␈α⊂so␈α∂improbable␈α⊂that␈α∂it␈α⊂is␈α∂hard␈α⊂to␈α∂take␈α⊂seriously␈α∂the
␈↓ α∧␈↓conditional␈α⊃probability␈α⊃of␈α∩a␈α⊃bridge␈α⊃given␈α⊃the␈α∩hypotheses.␈α⊃ Moreover,␈α⊃we␈α⊃mentally␈α∩propose␈α⊃to
␈↓ α∧␈↓ourselves␈α→the␈α→normal␈α→non-bridge␈α→non-sea␈α→monster␈α→interpretation␈α→␈↓↓before␈↓␈α→considering␈α_these
␈↓ α∧␈↓extraneous␈α
possibilities,␈α
let␈α
alone␈α
their␈α
probabilities,␈α
i.e.␈α
we␈α
usually␈α
don't␈α
even␈α
introduce␈α
the␈α
sample
␈↓ α∧␈↓space␈αin␈αwhich␈αthese␈αpossibilities␈αare␈αassigned␈αwhatever␈αprobabilities␈αone␈αmight␈αconsider␈αthem␈αto
␈↓ α∧␈↓have.␈α Therefore,␈αregardless␈αof␈αour␈αknowledge␈αof␈αprobabilities,␈αwe␈αneed␈αa␈αway␈αof␈αformulating␈αthe
␈↓ α∧␈↓normal␈α
situation␈α
from␈α
the␈α
statement␈α
of␈α
the␈α
facts,␈α
and␈α
the␈α
minimal␈α
completion␈α
axioms␈α
seems␈α
to␈α
be␈α
a
␈↓ α∧␈↓method.
␈↓ α∧␈↓␈↓ αTOf␈αcourse,␈αwe␈αhaven't␈αgiven␈αan␈αexpression␈αof␈αcommon␈αsense␈αknowledge␈αin␈αa␈αform␈αthat␈αsays
␈↓ α∧␈↓a␈α∂boat␈α∂can␈α⊂be␈α∂used␈α∂to␈α⊂cross␈α∂rivers␈α∂unless␈α∂there␈α⊂is␈α∂something␈α∂wrong␈α⊂with␈α∂it.␈α∂ In␈α⊂particular,␈α∂we
␈↓ α∧␈↓haven't␈α⊂introduced␈α⊂into␈α∂our␈α⊂␈↓↓ontology␈↓␈α⊂(the␈α∂things␈α⊂that␈α⊂exist)␈α∂a␈α⊂category␈α⊂that␈α⊂includes␈α∂␈↓↓something
␈↓ α∧␈↓↓wrong␈αwith␈αa␈αboat␈↓␈α
or␈αa␈αcategory␈αthat␈α
includes␈α␈↓↓something␈αthat␈αmay␈α
prevent␈αits␈αuse␈↓.␈α I␈α
imagine␈αthat
␈↓ α∧␈↓many␈α
philosophers␈α
and␈α
scientists␈α∞would␈α
be␈α
reluctant␈α
to␈α
introduce␈α∞such␈α
␈↓↓things,␈↓␈α
but␈α
the␈α∞fact␈α
that
␈↓ α∧␈↓ordinary␈α
language␈α
allows␈α
␈↓↓"something␈α
wrong␈α
with␈α
the␈α
boat"␈↓␈α
suggests␈α
that␈α
we␈α
shouldn't␈α
be␈α
hasty␈αin
␈↓ α∧␈↓excluding␈α∪it.␈α∀ Making␈α∪a␈α∪suitable␈α∀formalism␈α∪may␈α∪be␈α∀technically␈α∪difficult␈α∀and␈α∪philosophically
␈↓ α∧␈↓problematical, but we must try.
␈↓ α∧␈↓␈↓ αTIn␈α
compensation,␈αwe␈α
may␈α
get␈αan␈α
increased␈αability␈α
to␈α
understand␈αnatural␈α
language,␈αbecause␈α
if
␈↓ α∧␈↓natural␈αlanguage␈αadmits␈αsomething␈αlike␈αminimal␈αreasoning,␈αit␈αis␈αunderstandable␈αthat␈αwe␈αwill␈αhave
␈↓ α∧␈↓difficulty in translating it into logical formalisms that don't.
␈↓ α∧␈↓␈↓ ε|5␈↓ ∧
␈↓ α∧␈↓␈↓ εddraft␈↓ u6
␈↓ α∧␈↓αMinimal models and minimal entailment in propositional calculus.
␈↓ α∧␈↓␈↓ αTAs␈α⊗the␈α⊗above␈α⊗indicates,␈α⊗developing␈α⊗techniques␈α⊗for␈α⊗minimal␈α⊗entailment␈α⊗and␈α⊗minimal
␈↓ α∧␈↓inference␈αand␈αaxiomatizing␈αcommon␈αsense␈αknowledge␈αin␈αa␈αform␈αsuitable␈αfor␈αcomputer␈αuse␈αwill␈αbe
␈↓ α∧␈↓difficult.␈α Therefore␈α
it␈αseems␈αworthwhile␈α
to␈αstudy␈αa␈α
propositional␈αcalculus␈αanalog␈α
of␈αthe␈αfirst␈α
order
␈↓ α∧␈↓logic situation even though we haven't found any direct applications of the propositional case.
␈↓ α∧␈↓␈↓ αTSuppose␈α
we␈α
have␈α
some␈α
facts␈α
to␈α
express␈α
but␈α
have␈α
not␈α
yet␈α
chosen␈α
a␈α∞propositional␈α
language.
␈↓ α∧␈↓Our␈α⊂first␈α⊃step␈α⊂is␈α⊃to␈α⊂introduce␈α⊃propositional␈α⊂letters␈α⊃␈↓↓p␈↓β1␈↓↓,...,p␈↓βn␈↓␈α⊂and␈α⊃to␈α⊂specify␈α⊃each␈α⊂of␈α⊃them␈α⊂as
␈↓ α∧␈↓expressing␈α⊃some␈α⊃elementary␈α⊂fact.␈α⊃ We␈α⊃call␈α⊃this␈α⊂establishing␈α⊃a␈α⊃␈↓↓propositional␈α⊃co-ordinate␈α⊂system␈↓.
␈↓ α∧␈↓Then␈αwe␈αexpress␈αthe␈αset␈α␈↓↓A␈↓␈αof␈αknown␈αfacts␈αas␈αa␈αsentence␈α␈↓↓AX␈↓␈αin␈αthis␈αco-ordinate␈αsystem.␈α A␈αmodel
␈↓ α∧␈↓of␈αthe␈αfacts␈αis␈αany␈αassignment␈αof␈αtruth␈αvalues␈αto␈αthe␈α␈↓↓p␈↓βi␈↓'s␈αthat␈αmakes␈α␈↓↓AX␈↓␈αtrue.␈α Let␈α␈↓↓M1␈↓␈αand␈α␈↓↓M2␈↓␈αbe
␈↓ α∧␈↓models of ␈↓↓AX.␈↓ We define
␈↓ α∧␈↓␈↓ αT␈↓↓M1 ≤ M2 ≡ ∀i.(true(p␈↓βi␈↓↓,M2) ⊃ true(p␈↓βi␈↓↓,M1))␈↓.
␈↓ α∧␈↓A␈α
minimal␈α
model␈α
is␈α
one␈α
that␈α
is␈α
not␈αa␈α
proper␈α
extension,␈α
i.e.␈α
a␈α
model␈α
in␈α
which␈α
(roughly␈αspeaking)␈α
as
␈↓ α∧␈↓many␈αof␈α
the␈α␈↓↓p␈↓βi␈↓s␈αas␈α
possible␈αare␈αfalse␈α
-␈αconsistent␈α
with␈αthe␈αtruth␈α
of␈α␈↓↓AX␈↓.␈α ␈↓↓Note␈α
that␈αwhile␈αthe␈α
models
␈↓ α∧␈↓↓of␈αa␈αset␈αof␈αfacts␈αare␈αindependent␈αof␈αthe␈αco-ordinate␈αsystem,␈αthe␈αminimal␈αmodels␈αdepend␈αon␈αthe␈αco-
␈↓ α∧␈↓↓ordinate␈αsystem␈↓.␈α Here␈αis␈αthe␈αmost␈αtrivial␈αexample.␈α Let␈αthere␈αbe␈αone␈αletter␈α␈↓↓p␈↓␈αrepresenting␈αthe␈αone
␈↓ α∧␈↓fact␈α∞in␈α
a␈α∞co-ordinate␈α
system␈α∞␈↓↓C,␈↓␈α
and␈α∞let␈α
␈↓↓A␈↓␈α∞be␈α
the␈α∞null␈α
set␈α∞of␈α
facts␈α∞so␈α
that␈α∞␈↓↓AX␈↓␈α
is␈α∞the␈α∞sentence␈α
␈↓↓T␈↓
␈↓ α∧␈↓(identically␈α⊂true).␈α⊂ The␈α⊂one␈α⊂other␈α⊂co-ordinate␈α⊂system␈α⊂␈↓↓C'␈↓␈α⊂uses␈α⊂the␈α⊂elementary␈α⊂sentence␈α⊂␈↓↓p'␈↓␈α⊂taken
␈↓ α∧␈↓equivalent␈α
to␈α
␈↓↓¬p␈↓.␈α
The␈α
minimal␈α
model␈α
of␈α
␈↓↓C␈↓␈α
is␈α
{¬p},␈α
and␈α
the␈α
minimal␈α
model␈α
of␈α
␈↓↓C'␈↓␈α
is␈α
{p}.␈α Since
␈↓ α∧␈↓minimal␈α∞reasoning␈α
depends␈α∞on␈α
the␈α∞co-ordinate␈α
system␈α∞and␈α
not␈α∞merely␈α
on␈α∞the␈α
facts␈α∞expressed␈α
in
␈↓ α∧␈↓the␈αaxioms,␈αthe␈αutility␈αof␈αan␈αaxiom␈αsystem␈αwill␈αdepend␈αon␈αwhether␈αits␈αminimal␈αmodels␈αexpress␈α
the
␈↓ α∧␈↓uses we wish to make of Occam's razor.
␈↓ α∧␈↓␈↓ αTA␈α∪less␈α∩trivial␈α∪example␈α∩of␈α∪minimal␈α∩entailment␈α∪is␈α∩the␈α∪following.␈α∩ The␈α∪propositional␈α∩co-
␈↓ α∧␈↓ordinate␈α
system␈α∞has␈α
basic␈α
sentences␈α∞␈↓↓p␈↓β1␈↓,␈α
␈↓↓p␈↓β2␈↓␈α
and␈α∞␈↓↓p␈↓β3␈↓,␈α
and␈α
␈↓↓AX␈α∞=␈α
p␈↓β1␈↓↓␈α
∨␈α∞p␈↓β2␈↓.␈α
There␈α
are␈α∞two␈α
minimal
␈↓ α∧␈↓models.␈α
␈↓↓p␈↓β3␈↓␈α
is␈α
false␈αin␈α
both,␈α
and␈α
␈↓↓p␈↓β1␈↓␈αis␈α
false␈α
in␈α
one,␈αand␈α
␈↓↓p␈↓β2␈↓␈α
is␈α
false␈αin␈α
the␈α
other.␈α
Thus␈α
we␈αhave
␈↓ α∧␈↓␈↓↓AX ␈↓πq␈↓βm␈↓↓ (¬(p␈↓β1␈↓↓ ∧ p␈↓β2␈↓↓) ∧ ¬p␈↓β3␈↓).
␈↓ α∧␈↓␈↓ αTNote␈α
that␈αif␈α
␈↓↓AX␈↓␈αis␈α
a␈α
conjunction␈αof␈α
certain␈αelementary␈α
sentences␈α
(some␈αof␈α
them␈αnegated),␈α
e.g.
␈↓ α∧␈↓␈↓↓AX = p␈↓β2␈↓↓ ∧ ¬p␈↓β4␈↓,␈α∂then␈α∂there␈α∂is␈α∂a␈α∂unique␈α∂minimal␈α∂model,␈α∂but␈α∂if,␈α∂as␈α∂above,␈α∂␈↓↓AX = p␈↓β2␈↓↓ ∨ ¬p␈↓β4␈↓,␈α∂then
␈↓ α∧␈↓there is more than one minimal model.
␈↓ α∧␈↓␈↓ αTOne may also consider extensions ␈↓↓relative␈↓ to a set ␈↓↓B␈↓ of elementary sentences. We have
␈↓ α∧␈↓␈↓ αT␈↓↓M1 ≤ M2 (mod B) ≡ ∀p.(p ε B ∧ true(p,M1) ⊃ true(p,M2)␈↓.
␈↓ α∧␈↓We␈α⊂can␈α⊂then␈α⊂introduce␈α⊂minimal␈α⊂models␈α⊂relative␈α⊂to␈α⊂␈↓↓B␈↓␈α⊂and␈α⊂the␈α⊂corresponding␈α⊂relative␈α∂minimal
␈↓ α∧␈↓entailment.␈α
Thus␈α
we␈α
may␈α
care␈α
about␈α
minimality␈α∞and␈α
Occam's␈α
razor␈α
only␈α
over␈α
a␈α
certain␈α∞part␈α
of
␈↓ α∧␈↓our knowledge.
␈↓ α∧␈↓␈↓ αTNote␈α⊂that␈α⊂we␈α⊂may␈α⊂discover␈α⊂a␈α⊂set␈α⊂of␈α⊂facts␈α⊂one␈α⊂at␈α⊂a␈α⊂time␈α⊂so␈α⊂that␈α⊂we␈α⊂have␈α⊂an␈α⊂increasing
␈↓ α∧␈↓sequence␈α⊂␈↓↓A␈↓β1␈↓↓␈α⊂⊂␈α⊂A␈↓β2␈↓␈α⊂⊂␈α⊂...␈α⊂of␈α⊂sets␈α⊂of␈α⊂sentences.␈α⊂ A␈α⊂given␈α⊂sentence␈α⊂␈↓↓p␈↓␈α⊂may␈α⊂oscillate␈α⊂in␈α⊃its␈α⊂minimal
␈↓ α∧␈↓entailment␈α∞by␈α∞the␈α∞␈↓↓A␈↓βi␈↓,␈α
e.g.␈α∞we␈α∞may␈α∞have␈α
␈↓↓A␈↓β1␈↓π q␈↓βm␈↓↓ p␈↓,␈α∞␈↓↓A␈↓β2␈↓π q␈↓βm␈↓↓ ¬p␈↓,␈α∞neither␈α∞may␈α
be␈α∞entailed␈α∞by␈α∞␈↓↓A␈↓β3␈↓,␈α
etc.
␈↓ α∧␈↓␈↓ ε|6␈↓ ∧
␈↓ α∧␈↓␈↓ εddraft␈↓ u7
␈↓ α∧␈↓The␈α
common␈α∞sense␈α
Occam's␈α∞razor␈α
conclusion␈α
about␈α∞a␈α
sentence␈α∞␈↓↓p␈↓␈α
often␈α
behaves␈α∞this␈α
way␈α∞as␈α
our
␈↓ α∧␈↓knowledge increases.
␈↓ α∧␈↓␈↓ ε|7␈↓ ∧
␈↓ α∧␈↓␈↓ εddraft␈↓ u8
␈↓ α∧␈↓αNOTES
␈↓ α∧␈↓␈↓ αT1.␈α
There␈α
is␈α∞a␈α
relation␈α
between␈α∞minimal␈α
entailment␈α
and␈α∞the␈α
THNOT␈α
formalism␈α∞of␈α
micro-
␈↓ α∧␈↓planner.␈α (THNOT␈α␈↓↓p)␈↓␈αmeans␈αthat␈αan␈αattempt␈αto␈αprove␈α␈↓↓p␈↓␈αhas␈αfailed,␈αand␈αsuch␈αa␈αfailure␈α
to␈αprove
␈↓ α∧␈↓something␈αwrong␈α
with␈αthe␈αboat␈α
could␈αlead␈αto␈α
a␈αplan␈αto␈α
row␈αacross␈αthe␈α
river.␈α Likewise␈α
failure␈αto
␈↓ α∧␈↓prove the existence of a bridge can be used to go from the facts to the Amarel representation.
␈↓ α∧␈↓␈↓ αT2.␈αWhen␈α
we␈αadd␈α
common␈αsense␈αknowledge␈α
or␈αgeneral␈α
scientific␈αknowledge␈α
to␈αthe␈αfacts␈α
about
␈↓ α∧␈↓a␈α∩particular␈α∩problem,␈α∩we␈α∩get␈α⊃a␈α∩huge␈α∩collection␈α∩of␈α∩facts␈α⊃with␈α∩huge␈α∩models␈α∩most␈α∩of␈α∩which␈α⊃is
␈↓ α∧␈↓irrelevant␈αto␈αthe␈αproblem.␈α
The␈αusual␈αapproach␈αis␈α
for␈αthe␈αhuman␈αto␈α
separate␈αwhat␈αis␈αrelevant␈α
and
␈↓ α∧␈↓make␈αan␈αaxiom␈αsystem␈αcontaining␈αonly␈α
relevant␈αinformation.␈α If␈αwe␈αwant␈αa␈αcomputer␈α
program␈αto
␈↓ α∧␈↓express␈α∞what␈α∂it␈α∞knows␈α∞in␈α∂a␈α∞certain␈α∞language,␈α∂we␈α∞need␈α∞a␈α∂better␈α∞way.␈α∞ One␈α∂way␈α∞of␈α∂reducing␈α∞the
␈↓ α∧␈↓number␈αof␈α
models␈αis␈αto␈α
say␈αthat␈α
two␈αmodels␈αare␈α
equivalent␈αif␈α
they␈αare␈αthe␈α
same␈αfor␈α
certain␈αsorts
␈↓ α∧␈↓and␈αcertain␈αpredicates␈αand␈αfunctions.␈α We␈αthen␈α
work␈αwith␈αthe␈αequivalence␈αclasses␈αand␈αtry␈αto␈α
make
␈↓ α∧␈↓a␈α∞set␈α∞of␈α
sentences␈α∞involving␈α∞only␈α
the␈α∞objects␈α∞in␈α∞these␈α
sorts␈α∞and␈α∞as␈α
few␈α∞others␈α∞as␈α∞possible␈α
whose
␈↓ α∧␈↓models correspond to these equivalence classes.
␈↓ α∧␈↓␈↓ αT3.␈αIn␈αthe␈αfirst␈αorder␈α
logic␈αtheory␈αwe␈αalso␈αneed␈α
to␈αconsider␈αextensions␈αand␈αminimality␈α
relative
␈↓ α∧␈↓to a subcollection of the sorts.
␈↓ α∧␈↓␈↓ αT4.␈α∂In␈α∂the␈α∂propositional␈α∂calculus␈α∂system␈α∂we␈α∂minimize␈α∂the␈α∂set␈α∂of␈α⊂propositional␈α∂co-ordinates
␈↓ α∧␈↓assigned␈α∂␈↓αtrue␈↓␈α∂while␈α∞in␈α∂the␈α∂predicate␈α∂calculus␈α∞system␈α∂we␈α∂minimize␈α∂the␈α∞set␈α∂of␈α∂objects␈α∂asserted␈α∞to
␈↓ α∧␈↓exist.␈α
It␈α
might␈α
be␈α
worth␈α
considering␈α
co-ordinate␈α
systems␈α
in␈α
the␈α
predicate␈α
calculus␈α
system␈α
within
␈↓ α∧␈↓which it is worthwhile to minimize the set of propositions asserted.
␈↓ α∧␈↓John McCarthy
␈↓ α∧␈↓Artificial Intelligence Laboratory
␈↓ α∧␈↓Stanford University
␈↓ α∧␈↓Stanford, California 94305
␈↓ α∧␈↓␈↓εThis draft PUBbed at 15:34 on December 1, 1976.
␈↓ α∧␈↓␈↓ ε|8␈↓ ∧